The present invention is related to satisfiability problems. More particularly, the present invention is directed to a method and system for solving satisfiability problems.
The satisfiability (SAT) problem consists of determining a satisfying variable assignment, V, for a function (or formula), ƒ, or determining that no such V exists. The function ƒ may be expressed in conjunctive normal form (CNF), which consists of the logical AND (i.e., conjunction) of one or more clauses. Each clause consists of the logical OR (i.e., disjunction) of one or more literals. A literal is a Boolean function of one argument or variable. Each variable x has a positive literal, i.e., the identity function of x, denoted as x, and a negative literal, i.e., the negation function of x, denoted as ˜x.
One solution to the satisfiability problem is to search through all possible assignments. However, with n variables, there are 2n possible assignments. Therefore, as the number of variables grows, the number of possible assignments to search through increases exponentially. This can make finding a solution very difficult. Since many problems in synthesis, automatic test pattern generation (ATPG), verification, artificial intelligence, cryptology, and other fields reduce to SAT problems, it is desirable to discover new methods and systems for solving SAT problems efficiently.
Some of the SAT-algorithms that have been developed include GRASP, SATO, and Chaff, which are described in J. P. M. Silva and K. A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions of Computers, volume 48, pages 506-521, 1999, H. Zhang, SATO: An efficient propositional prover, Proceedings of the International Conference on Automated Deduction, pages 272-275, July 1997, and M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver, Proceeding of the 38th Design Automation Conference, 2001. All of these are search algorithms aimed at finding a satisfying assignment by variable splitting. Search algorithms of that kind are descendants of the Davis-Putnam-Loveland-Longemann (DPLL) algorithm, which is described in M. Davis, G. Longemann, and D. Loveland, A Machine program for theorem proving, Communications of the ACM, volume 5, pages 394-397, 1962.
When looking for a solution, the DPLL-algorithm examines a search tree. This tree-like search can be considered as an implementation of the tree-like resolution proof system which is a special case of general resolution. It was shown in E. Ben-Sasson, R. Impagliazzo, and A. Wigderson, Near optimal separation of Treelike and General resolution, Proceedings of SAT-2000: Third Workshop on the Satisfiability Problem, pages 14-18, May 2000, that there is an exponential gap between the performance of tree-like resolution and that of general resolution.
Search algorithms, such as GRASP, SATO, and Chaff, have made steps towards general resolution by trying to eliminate the drawbacks and limitations of pure tree-like resolution. For example, these SAT-solvers record conflict clauses, which are implicates of the original formula. Adding conflict clauses allows for pruning of many branches of the search tree that have yet to be examined. The deduced implicates are added to a clause database.
In addition, some of the SAT-algorithms use the strategy of restarts. A restart is when the SAT-algorithm abandons the current search tree (without completing it) and starts a new one. So instead of one complete search tree, a set of incomplete trees (except the last one) are constructed. In L. Baptista and J. P. Marques-Silva, The interplay of randomization and learning on real-world instances of satisfiability, Proceedings of AAAI Workshop on Leveraging Probability and Uncertainty in Computation, July 2000 and C. P. Gomes, B. Selman, and H. Kautz, Boosting combinational search through randomization, Proceedings of International Conference on Principles and Practice of Constraint Programming, 1997, the usefulness of restarts was proven experimentally.
Although current SAT-solvers have made substantial progress towards general resolution, much still needs to be done to improve performance and robustness. For example, there are formulas that can be finished in a few seconds by one SAT-solver, but cannot be solved by another SAT-solver. This suggests that these SAT-solvers are not robust, e.g., these SAT-solvers either solve a formula quickly or not at all regardless of how much time they are given to find a solution. Additionally, current SAT-solvers are not flexible enough to take into account a formula's structure. In many cases, this results in poor performance and lack of robustness, e.g., substantial change in performance occurs after the formula is slightly changed.
Some of the current SAT-solvers use the activity of variables in conflict making to single out good candidates for branching variables. They compute the activity of a variable by counting the number of occurrences of literals of each variable in conflict clauses. Separate counters are maintained for each literal. By only taking into account the occurrences of variables in conflict clauses, there may not be an accurate estimate of the activity of some variables. In particular, the variables that actively contribute to conflicts but do not appear in conflict clauses may be overlooked. For instance, if a variable is frequently assigned through deduction, it may drive many conflicts without appearing in conflict clauses. Therefore, if only conflict clauses are taken into account when computing the activity of the variable, this activity will be underestimated.
Additionally, some SAT-solvers periodically divide the activity counters by a small constant. This strategy may not be able to adjust quickly enough to changes in the set of relevant variables. For example, suppose activity counters are divided by 2 every 100 conflicts and suppose that immediately after dividing the counters, a change of relevant variables occurs. Then, for the next 20-30 conflicts, the choice of branching variables will be dominated by an obsolete set of active variables.
Moreover, current SAT-solvers examine the whole set of variables each time they select a branching variable. This may be inefficient when there is a large number of variables in the set. Further, some of the current SAT-solvers remove conflict clauses based solely on the size (or length) of the conflict clause, i.e., the number of literals in the clause. However, some conflict clauses that have a sizeable number of literals may be more useful than conflict clauses with less literals. Consequently, removing conflict clauses simply based on size may be unwise. Other SAT-solvers remove conflict clauses whenever the memory is full. Not only is this inefficient, it may also lead to the removal of useful conflict clauses.
The present invention provides a method and system for solving satisfiability problems. In one embodiment, a plurality of clauses in a satisfiability problem are organized as a chronologically ordered stack. The stack has a top and a bottom and newly deduced conflict clauses are added to the top of the stack. A branching variable is then selected from a plurality of unassigned variables in the CNF formula and the selected branching variable is assigned a value of 0 or 1. One or more clauses are marked as satisfied, and Boolean Constraint Propagation is invoked when the stack contains one or more unit clauses. The process of making value assignment to branching variables (accompanied by invoking Boolean Constraint Propagation) goes on until one of the following two conditions hold. If all the clauses of the stack are satisfied, the accumulated set of variable assignments is returned as a solution. The second condition is that a clause which is unsatisfiable under the current set of assignments is produced. In that case, a new clause is learned and added to the stack. After that, a subset of last assignments is undone and new assignments to branching variables followed by Boolean Constraint Propagation are made. This goes on until an empty clause is derived (the initial formula is unsatisfiable) or a solution is found (the initial formula is satisfiable).
Further details of aspects, objects, and advantages of the invention are described below in the detailed description, drawings, and claims. Both the foregoing general description and the following detailed description are exemplary and explanatory, and are not intended to be limiting as to the scope of the invention.